<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
	<head>
		<title>The Lattice of Kinds</title>
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
		<meta name="viewport" content="width=device-width initial-scale=1">
		<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
		<meta http-equiv="Content-Language" content="en-gb">

<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
<script>
MathJax = {
	tex: {
		inlineMath: '$', '$'], ['\\(', '\\)'
	},
	svg: {
		fontCache: 'global'
	}
};
</script>
<script type="text/javascript" id="MathJax-script" async
	src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
</script>

<script>
function togglePopup(material_id) {
  var popup = document.getElementById(material_id);
  popup.classList.toggle("show");
}
</script>

<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
<script src="http://code.jquery.com/jquery-1.12.4.min.js"
	integrity="sha256-ZosEbRLbNQzLpnKIkEdrPv7lOy9C27hHQ+Xp8a4MxAQ=" crossorigin="anonymous"></script>

<script src="../docs-assets/Bigfoot.js"></script>
<link href="../docs-assets/Bigfoot.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
		
	</head>
	<body class="commentary-font">
		<nav role="navigation">
		<h1><a href="../index.html"><img src="../docs-assets/Inform.png" height=72> </a></h1>
<ul><li><a href="../index.html">home</a></li>
</ul><h2>Compiler</h2><ul>
<li><a href="../structure.html">structure</a></li>
<li><a href="../inbuildn.html">inbuild</a></li>
<li><a href="../inform7n.html">inform7</a></li>
<li><a href="../intern.html">inter</a></li>
<li><a href="../services.html">services</a></li>
<li><a href="../secrets.html">secrets</a></li>
</ul><h2>Other Tools</h2><ul>
<li><a href="../inblorbn.html">inblorb</a></li>
<li><a href="../inform6.html">inform6</a></li>
<li><a href="../inpolicyn.html">inpolicy</a></li>
</ul><h2>Resources</h2><ul>
<li><a href="../extensions.html">extensions</a></li>
<li><a href="../kits.html">kits</a></li>
</ul><h2>Repository</h2><ul>
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=0> github</a></li>
</ul><h2>Related Projects</h2><ul>
<li><a href="https://github.com/ganelson/inweb"><img src="../docs-assets/github.png" height=0> inweb</a></li>
<li><a href="https://github.com/ganelson/intest"><img src="../docs-assets/github.png" height=0> intest</a></li>
</ul>
		</nav>
		<main role="main">
		<!-- Weave of 'The Lattice of Kinds' generated by inweb -->
<div class="breadcrumbs">
    <ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../services.html">Services</a></li><li><a href="index.html">kinds</a></li><li><a href="index.html#2">Chapter 2: Kinds</a></li><li><b>The Lattice of Kinds</b></li></ul></div>
<p class="purpose">Placing a partial order on kinds according to whether one conforms to another.</p>

<ul class="toc"><li><a href="2-tlok.html#SP1">&#167;1. Conformance</a></li><li><a href="2-tlok.html#SP6">&#167;6. Lattice operations</a></li><li><a href="2-tlok.html#SP8">&#167;8. Compatibility</a></li><li><a href="2-tlok.html#SP13">&#167;13. Common code</a></li></ul><hr class="tocbar">

<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>&#167;1. Conformance.</b>If we write \(K\leq L\) to mean that \(K\) conforms to \(L\), then \(\leq\) provides
an ordering on kinds. For any kinds \(K, L, M\) not making use of kind variables<sup id="fnref:1"><a href="#fn:1" rel="footnote">1</a></sup>
it is true that:
</p>

<ul class="items"><li>&#9679; \(K \leq K\) &mdash; reflexivity.
</li><li>&#9679; If \(K\leq L\) and \(L\leq M\) then \(K\leq M\) &mdash; transitivity.
</li><li>&#9679; <span class="extract"><span class="extract-syntax">K_nil</span></span> \(\leq K \leq\) <span class="extract"><span class="extract-syntax">value</span></span> &mdash; there are top and bottom elements.<sup id="fnref:2"><a href="#fn:2" rel="footnote">2</a></sup>
</li><li>&#9679; If \(K \leq L\) then a value of kind \(K\) can always be substituted for a
value of kind \(L\) without modification &mdash; the Liskov substitution principle.<sup id="fnref:3"><a href="#fn:3" rel="footnote">3</a></sup>
</li><li>&#9679; There is a join \(K\lor L\) and a meet \(K\land L\) such that
\(K\land L\leq K, L\leq K\lor L\), where \(K\lor L\) is minimal and \(K\land L\)
maximal with that property.
</li></ul>
<ul class="footnotetexts"><li class="footnote" id="fn:1"><p class="inwebfootnote"><sup id="fnref:1"><a href="#fn:1" rel="footnote">1</a></sup> Introducing kind variables complicates the picture, because whether or not
<span class="extract"><span class="extract-syntax">list of K</span></span> conforms to <span class="extract"><span class="extract-syntax">list of arithmetic values</span></span> depends on the current
value of <span class="extract"><span class="extract-syntax">K</span></span> and therefore on the current context.
<a href="#fnref:1" title="return to text"> &#x21A9;</a></p></li><li class="footnote" id="fn:2"><p class="inwebfootnote"><sup id="fnref:2"><a href="#fn:2" rel="footnote">2</a></sup> <span class="extract"><span class="extract-syntax">K_nil</span></span> is a kind which exists only for kind-checking purposes, meaning
"a member of the empty set". Clearly no value can ever have this. This
differs from <span class="extract"><span class="extract-syntax">K_void</span></span>, which means "the absence of a value". Neither can ever
be the kind of a variable, of course.
<a href="#fnref:2" title="return to text"> &#x21A9;</a></p></li><li class="footnote" id="fn:3"><p class="inwebfootnote"><sup id="fnref:3"><a href="#fn:3" rel="footnote">3</a></sup> Also known as strong behavioural subtyping. This only applies to definite
kinds, because no value ever has an indefinite kind.
<a href="#fnref:3" title="return to text"> &#x21A9;</a></p></li></ul>
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>&#167;2. </b>In general there is no guarantee of antisymmetry, i.e., that \(K\leq L\)
and \(L\leq K\) must mean \(K = L\), nor that \(K\lor L\) or \(K\land L\) are unique.
We could imagine creating indefinite kinds <span class="extract"><span class="extract-syntax">rhyming with lumber value</span></span> and
<span class="extract"><span class="extract-syntax">calculator value</span></span> such that <span class="extract"><span class="extract-syntax">number</span></span> and <span class="extract"><span class="extract-syntax">real number</span></span> would conform to both.
If so, then either one of <span class="extract"><span class="extract-syntax">rhyming with lumber value</span></span> and <span class="extract"><span class="extract-syntax">calculator value</span></span>
could equally well serve as \(K\lor L\). The set of kinds is therefore not
formally a lattice.
</p>

<p class="commentary">As it happens, however, Inform's choice of indefinite kinds is made in
such a way that this does not happen. The upshot is that although the set of
kinds is not necessarily a lattice, it often will be in practice, and we use
the language of lattices &mdash; hence, words like "join" and "meet" &mdash; as a guide.
</p>

<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>&#167;3. </b>Conformance is tested with the function <a href="2-knd.html#SP28" class="internal">Kinds::conforms_to</a>, and the
following shows it in action.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new kind thing of object</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new kind device of thing</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new kind vehicle of thing</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new unit length</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">number &lt;= number?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">number &lt;= real number?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">value &lt;= number?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">object &lt;= text?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">object &lt;= thing?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">thing &lt;= object?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">device &lt;= thing?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">device &lt;= object?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">list of devices &lt;= thing?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">list of devices &lt;= list of things?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
</pre>
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>&#167;4. </b>The indefinite <span class="extract"><span class="extract-syntax">arithmetic kind</span></span> used by Inform is a good example of what
in other languages would be called a protocol. Here we see conformance:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new unit length</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">number &lt;= arithmetic value?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">real number &lt;= arithmetic value?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">length &lt;= arithmetic value?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">text &lt;= arithmetic value?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">arithmetic value &lt;= value?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">value &lt;= arithmetic value?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">arithmetic value &lt;= sayable value?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
</pre>
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>&#167;5. </b>Here we see covariance versus contravariance:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new kind larger of object</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new kind smaller of larger</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">smaller &lt;= larger?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">larger &lt;= smaller?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">list of smaller &lt;= list of larger?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">list of larger &lt;= list of smaller?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">relation of larger to texts &lt;= relation of smaller to texts?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">relation of smaller to texts &lt;= relation of larger to texts?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">phrase larger -&gt; text &lt;= phrase smaller -&gt; text?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">phrase smaller -&gt; text &lt;= phrase larger -&gt; text?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">phrase text -&gt; larger &lt;= phrase text -&gt; smaller?</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">phrase text -&gt; smaller &lt;= phrase text -&gt; larger?</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
</pre>
<ul class="items"><li>&#9679; A constructor \(\phi\) is "covariant" &mdash; meaning, goes the same way &mdash; if
\(K\leq L\) means \(\phi(K)\leq\phi(L)\).
</li><li>&#9679; It is "contravariant" &mdash; goes the opposite way &mdash; if \(K\leq L\) means
\(\phi(L)\leq\phi(K)\).
</li></ul>
<p class="commentary">Note that "list of ..." is covariant; "phrase ... -&gt; ..." is contravariant in
the first term, but covariant in the second. To see why, consider a function
\(f: K\to L\), and then considering expanding or contracting the sets \(K\) and \(L\).
It's no problem if \(L\) grows larger &mdash; \(f\) can still be used &mdash; but if \(L\)
shrinks then \(f\) might map outside it, which is unsafe. But the reverse is true
for \(K\). If \(K\) shrinks we can still use \(f\), but if it grows then we may not
be able to. If \(K_1\leq K\leq K_2\) and \(L_1\leq L\leq L_2\), then a function
\(f:K\to L\) is also a function \(K_1\to L_2\), but not \(K_2\to L_1\).
</p>

<p class="commentary">See <a href="2-tlok.html#SP13" class="internal">Latticework::order_relation</a> for more.
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">COVARIANT</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">CONTRAVARIANT</span><span class="plain-syntax"> -1</span>
</pre>
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>&#167;6. Lattice operations.</b>Every \(K\) other than <span class="extract"><span class="extract-syntax">value</span></span>, <span class="extract"><span class="extract-syntax">K_nil</span></span> and <span class="extract"><span class="extract-syntax">K_void</span></span> has a minimal element \(K^+\)
such that \(K\leq K^+\) but \(K\neq K^+\): we call this the "superkind" of \(K\).
Assuming kinds form a lattice, this will be unique. The following function
returns the superkind, or <span class="extract"><span class="extract-syntax">NULL</span></span> for special cases which do not have one.
</p>

<p class="commentary">It is in this function that the basic conformance facts are expressed. We
hard-code that for the built-in indefinite kinds, and give the client tool
a chance to provide other conformances. For Inform, for example, the callback
function is what tells us that the superkind of <span class="extract"><span class="extract-syntax">man</span></span> is <span class="extract"><span class="extract-syntax">person</span></span>.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">Latticework::super</span><button class="popup" onclick="togglePopup('usagePopup1')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup1">Usage of <span class="code-font"><span class="function-syntax">Latticework::super</span></span>:<br/><a href="2-tlok.html#SP7">&#167;7</a>, <a href="2-tlok.html#SP15">&#167;15</a><br/>Kinds - <a href="2-knd.html#SP24">&#167;24</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_real_arithmetic_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_arithmetic_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_enumerated_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_understandable_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_arithmetic_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_understandable_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_understandable_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_sayable_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_pointer_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_sayable_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_sayable_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_stored_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_stored_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_nil</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_void</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">HIERARCHY_GET_SUPER_KINDS_CALLBACK</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">S</span><span class="plain-syntax"> = </span><span class="identifier-syntax">HIERARCHY_GET_SUPER_KINDS_CALLBACK</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">S</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">S</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-kc2.html#SP24" class="function-link"><span class="function-syntax">KindConstructors::compatible</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_real_arithmetic_value</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_real_arithmetic_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-kc2.html#SP24" class="function-link"><span class="function-syntax">KindConstructors::compatible</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_enumerated_value</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_enumerated_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-kc2.html#SP24" class="function-link"><span class="function-syntax">KindConstructors::compatible</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_arithmetic_value</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_arithmetic_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-kc2.html#SP24" class="function-link"><span class="function-syntax">KindConstructors::compatible</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_pointer_value</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_pointer_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-kc2.html#SP24" class="function-link"><span class="function-syntax">KindConstructors::compatible</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_understandable_value</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_understandable_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-kc2.html#SP24" class="function-link"><span class="function-syntax">KindConstructors::compatible</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_sayable_value</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_sayable_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-kc2.html#SP24" class="function-link"><span class="function-syntax">KindConstructors::compatible</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_stored_value</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_stored_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>&#167;7. </b>Joins are defined above. So are meets, though in practice they are never useful
to us except as a way of calculating joins: the two are dual to each other as
they pass through contravariant constructors.
</p>

<p class="commentary">The main use of this for Inform is to handle literals such as:
</p>

<blockquote>
    <p>{ 1, 2.1415, "frog" }</p>
</blockquote>

<p class="commentary">The kind of this is by definition the join of the kinds of the values in the
list, which as it happens is <span class="extract"><span class="extract-syntax">K_sayable_value</span></span> &mdash; an indefinite kind, so that
such a list can't be constructed as data.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">Latticework::join</span><span class="plain-syntax">(</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K2</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="2-tlok.html#SP7" class="function-link"><span class="function-syntax">Latticework::j_or_m</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="identifier-syntax">K2</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">Latticework::meet</span><span class="plain-syntax">(</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K2</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="2-tlok.html#SP7" class="function-link"><span class="function-syntax">Latticework::j_or_m</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="identifier-syntax">K2</span><span class="plain-syntax">, -1);</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">Latticework::j_or_m</span><span class="plain-syntax">(</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K2</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">direction</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K1</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K2</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K2</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K1</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">kind_constructor</span><span class="plain-syntax"> *</span><span class="identifier-syntax">con</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K1</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">a1</span><span class="plain-syntax"> = </span><a href="4-kc2.html#SP17" class="function-link"><span class="function-syntax">KindConstructors::arity</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">con</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">a2</span><span class="plain-syntax"> = </span><a href="4-kc2.html#SP17" class="function-link"><span class="function-syntax">KindConstructors::arity</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K2</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">a1</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">a2</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K2</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax"> != </span><span class="identifier-syntax">con</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">ka</span><span class="plain-syntax">[</span><span class="constant-syntax">MAX_KIND_CONSTRUCTION_ARITY</span><span class="plain-syntax">] = { </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, };</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;</span><span class="identifier-syntax">a1</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">con</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">variance</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] == </span><span class="constant-syntax">COVARIANT</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">ka</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] = </span><a href="2-tlok.html#SP7" class="function-link"><span class="function-syntax">Latticework::j_or_m</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">K2</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">direction</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">else</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">ka</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] = </span><a href="2-tlok.html#SP7" class="function-link"><span class="function-syntax">Latticework::j_or_m</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">K2</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], -</span><span class="identifier-syntax">direction</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">a1</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="2-knd.html#SP9" class="function-link"><span class="function-syntax">Kinds::unary_con</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">con</span><span class="plain-syntax">, </span><span class="identifier-syntax">ka</span><span class="plain-syntax">[0]);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="2-knd.html#SP9" class="function-link"><span class="function-syntax">Kinds::binary_con</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">con</span><span class="plain-syntax">, </span><span class="identifier-syntax">ka</span><span class="plain-syntax">[0], </span><span class="identifier-syntax">ka</span><span class="plain-syntax">[1]);</span>
<span class="plain-syntax">    } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">        </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP7_1" class="named-paragraph-link"><span class="named-paragraph">Deal with nil</span><span class="named-paragraph-number">7.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP7_2" class="named-paragraph-link"><span class="named-paragraph">Deal with floating-point promotions</span><span class="named-paragraph-number">7.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP28" class="function-link"><span class="function-syntax">Kinds::conforms_to</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="identifier-syntax">K2</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> (</span><span class="identifier-syntax">direction</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)?</span><span class="identifier-syntax">K2:K1</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP28" class="function-link"><span class="function-syntax">Kinds::conforms_to</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K2</span><span class="plain-syntax">, </span><span class="identifier-syntax">K1</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> (</span><span class="identifier-syntax">direction</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)?</span><span class="identifier-syntax">K1:K2</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">direction</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K1</span><span class="plain-syntax">; </span><span class="identifier-syntax">K</span><span class="plain-syntax">; </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="2-tlok.html#SP6" class="function-link"><span class="function-syntax">Latticework::super</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">))</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP28" class="function-link"><span class="function-syntax">Kinds::conforms_to</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K2</span><span class="plain-syntax">, </span><span class="identifier-syntax">K</span><span class="plain-syntax">))</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_nil</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP7_1" class="paragraph-anchor"></a><b>&#167;7.1. </b>This ensures that \(K\land\) <span class="extract"><span class="extract-syntax">K_nil</span></span> \( = \) <span class="extract"><span class="extract-syntax">K_nil</span></span>, and that
\(K\lor\) <span class="extract"><span class="extract-syntax">K_nil</span></span> \( = K\).
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Deal with nil</span><span class="named-paragraph-number">7.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_nil</span><span class="plain-syntax">))) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> (</span><span class="identifier-syntax">direction</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)?</span><span class="identifier-syntax">K2:K1</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K2</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_nil</span><span class="plain-syntax">))) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> (</span><span class="identifier-syntax">direction</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)?</span><span class="identifier-syntax">K1:K2</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP7">&#167;7</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP7_2" class="paragraph-anchor"></a><b>&#167;7.2. </b>If one of \(K_1\), \(K_2\) uses floating-point and the other doesn't, then
we promote the one which doesn't before taking the join. This is useful
when inferring the kind of a constant list or column which mixes floating-point
and integer literals; recall that <span class="extract"><span class="extract-syntax">number</span></span> \(\not\leq\) <span class="extract"><span class="extract-syntax">real number</span></span>, so
without this promotion there would be no way to join such kinds.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Deal with floating-point promotions</span><span class="named-paragraph-number">7.2</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="3-fv.html#SP2" class="function-link"><span class="function-syntax">Kinds::FloatingPoint::uses_floating_point</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax">        (</span><a href="3-fv.html#SP2" class="function-link"><span class="function-syntax">Kinds::FloatingPoint::uses_floating_point</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K2</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax">        (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><a href="3-fv.html#SP1" class="function-link"><span class="function-syntax">Kinds::FloatingPoint::real_equivalent</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">), </span><span class="identifier-syntax">K2</span><span class="plain-syntax">)))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> (</span><span class="identifier-syntax">direction</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)?</span><span class="identifier-syntax">K2:K1</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="3-fv.html#SP2" class="function-link"><span class="function-syntax">Kinds::FloatingPoint::uses_floating_point</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K2</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax">        (</span><a href="3-fv.html#SP2" class="function-link"><span class="function-syntax">Kinds::FloatingPoint::uses_floating_point</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax">        (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><a href="3-fv.html#SP1" class="function-link"><span class="function-syntax">Kinds::FloatingPoint::real_equivalent</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K2</span><span class="plain-syntax">), </span><span class="identifier-syntax">K1</span><span class="plain-syntax">)))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> (</span><span class="identifier-syntax">direction</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)?</span><span class="identifier-syntax">K1:K2</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP7">&#167;7</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>&#167;8. Compatibility.</b>A related but different question is "compatibility". This asks whether a
value of kind \(K\) can be used where \(L\) is expected, but:
</p>

<ul class="items"><li>(i) It is now okay if explicit code to perform a conversion would be needed; and
</li><li>(ii) There are now three possible answers &mdash; always, never and sometimes, where
"sometimes" means that code can be compiled which would test compatibility at
run time rather than compile time.
</li></ul>
<p class="commentary">Conformance implies compatibility but not vice versa. For example:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new kind thing of object</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new kind device of thing</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new kind vehicle of thing</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new unit length</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">number compatible with number?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">number compatible with real number?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">value compatible with number?</span><span class="plain-syntax">':</span><span class="string-syntax"> never</span>
<span class="plain-syntax">'</span><span class="element-syntax">object compatible with text?</span><span class="plain-syntax">':</span><span class="string-syntax"> never</span>
<span class="plain-syntax">'</span><span class="element-syntax">object compatible with thing?</span><span class="plain-syntax">':</span><span class="string-syntax"> sometimes</span>
<span class="plain-syntax">'</span><span class="element-syntax">thing compatible with object?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">device compatible with thing?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">device compatible with object?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">list of devices compatible with thing?</span><span class="plain-syntax">':</span><span class="string-syntax"> never</span>
<span class="plain-syntax">'</span><span class="element-syntax">list of devices compatible with list of things?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">relation of things to texts compatible with relation of devices to texts?</span><span class="plain-syntax">':</span><span class="string-syntax"> never</span>
<span class="plain-syntax">'</span><span class="element-syntax">relation of devices to texts compatible with relation of things to texts?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">phrase thing -&gt; text compatible with phrase device -&gt; text?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">phrase device -&gt; text compatible with phrase thing -&gt; text?</span><span class="plain-syntax">':</span><span class="string-syntax"> never</span>
<span class="plain-syntax">'</span><span class="element-syntax">phrase text -&gt; thing compatible with phrase text -&gt; device?</span><span class="plain-syntax">':</span><span class="string-syntax"> never</span>
<span class="plain-syntax">'</span><span class="element-syntax">phrase text -&gt; device compatible with phrase text -&gt; thing?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">activity on numbers compatible with activity?</span><span class="plain-syntax">':</span><span class="string-syntax"> always</span>
<span class="plain-syntax">'</span><span class="element-syntax">first term of activity</span><span class="plain-syntax">':</span><span class="string-syntax"> nothing</span>
<span class="plain-syntax">'</span><span class="element-syntax">activity on numbers compatible with activity on values?</span><span class="plain-syntax">':</span><span class="string-syntax"> never</span>
</pre>
<p class="commentary">Note that <span class="extract"><span class="extract-syntax">number</span></span> is compatible with <span class="extract"><span class="extract-syntax">real number</span></span>. Run-time code will be
needed to convert the value, but the answer is "always". We also see that
<span class="extract"><span class="extract-syntax">device</span></span> is always compatible with <span class="extract"><span class="extract-syntax">thing</span></span> &mdash; every device is a thing &mdash;
but also that <span class="extract"><span class="extract-syntax">thing</span></span> is sometimes compatible with <span class="extract"><span class="extract-syntax">device</span></span>. If we pass a
thing to a function expecting to see a device, run-time code can check whether
the value passed is indeed a device, and reject the call with a run-time error
if not.
</p>

<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>&#167;9. </b>Kind checking can happen for many reasons, but the most difficult case
occurs when matching phrase prototypes. This is difficult because it involves
kind variables:
</p>

<blockquote>
    <p>To add (new entry - K) to (L - list of values of kind K) ...</p>
</blockquote>

<p class="commentary">This matches "add 23 to U" if "L" is a list of numbers, but not if it
is a list of times.
</p>

<p class="commentary">Since kind variables can be changed only when matching phrase prototypes,
and this is not a recursive process, we can store the current definitions
of A to Z in a single array.
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">MAX_KIND_VARIABLES</span><span class="plain-syntax"> </span><span class="constant-syntax">27</span><span class="plain-syntax"> </span><span class="comment-syntax"> we number them from 1 (A) to 26 (Z)</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">values_of_kind_variables</span><span class="plain-syntax">[</span><span class="constant-syntax">MAX_KIND_VARIABLES</span><span class="plain-syntax">];</span>
</pre>
<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>&#167;10. </b>In theory the kind-checker only needs to read the values of <span class="extract"><span class="extract-syntax">A</span></span> to <span class="extract"><span class="extract-syntax">Z</span></span>, not
to write them. If <span class="extract"><span class="extract-syntax">Q</span></span> is currently equal to <span class="extract"><span class="extract-syntax">number</span></span>, then it should check
kinds against <span class="extract"><span class="extract-syntax">Q</span></span> exactly as if it were checking against <span class="extract"><span class="extract-syntax">number</span></span>. It can
indeed do this &mdash; that's the <span class="extract"><span class="extract-syntax">MATCH_KIND_VARIABLES_AS_VALUES</span></span> mode. It can
also ignore the values of kind variables and treat them as names, so that
<span class="extract"><span class="extract-syntax">Q</span></span> matches only against <span class="extract"><span class="extract-syntax">Q</span></span>, regardless of its current value; that's the
<span class="extract"><span class="extract-syntax">MATCH_KIND_VARIABLES_AS_SYMBOLS</span></span> mode. Or it can match anything
against <span class="extract"><span class="extract-syntax">Q</span></span>, which is <span class="extract"><span class="extract-syntax">MATCH_KIND_VARIABLES_AS_UNIVERSAL</span></span> mode.
</p>

<p class="commentary">More interestingly, the kind-checker can also set the values of <span class="extract"><span class="extract-syntax">A</span></span> to <span class="extract"><span class="extract-syntax">Z</span></span>.
This is convenient since checking their correctness is more or less the same
thing as inferring what they seem to be in a given situation. So this is
<span class="extract"><span class="extract-syntax">MATCH_KIND_VARIABLES_INFERRING_VALUES</span></span> mode.
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">MATCH_KIND_VARIABLES_AS_SYMBOLS</span><span class="plain-syntax"> </span><span class="constant-syntax">0</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">MATCH_KIND_VARIABLES_INFERRING_VALUES</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">MATCH_KIND_VARIABLES_AS_VALUES</span><span class="plain-syntax"> </span><span class="constant-syntax">2</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">MATCH_KIND_VARIABLES_AS_UNIVERSAL</span><span class="plain-syntax"> </span><span class="constant-syntax">3</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">kind_checker_mode</span><span class="plain-syntax"> = </span><span class="constant-syntax">MATCH_KIND_VARIABLES_AS_SYMBOLS</span><span class="plain-syntax">;</span>
</pre>
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>&#167;11. </b>When the kind-checker does choose a value for a variable, it not only
sets the relevant entry in the above array but also creates a note that
this has been done. (If a phrase is correctly matched by the specification
matcher, a linked list of these notes is attached to the results: thus
a match of "add 23 to U" in the example above would produce a successful
result plus a note that <span class="extract"><span class="extract-syntax">K</span></span> has to be <span class="extract"><span class="extract-syntax">list of numbers</span></span>.)
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">typedef</span><span class="plain-syntax"> </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="reserved-syntax">kind_variable_declaration</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">kv_number</span><span class="plain-syntax">; </span><span class="comment-syntax"> must be from 1 to 26</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kv_value</span><span class="plain-syntax">; </span><span class="comment-syntax"> must be a definite non-</span><span class="extract"><span class="extract-syntax">NULL</span></span><span class="comment-syntax"> kind</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="reserved-syntax">kind_variable_declaration</span><span class="plain-syntax"> *</span><span class="identifier-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">CLASS_DEFINITION</span>
<span class="plain-syntax">} </span><span class="reserved-syntax">kind_variable_declaration</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>The structure kind_variable_declaration is accessed in 3/dmn and here.</li></ul>
<p class="commentary firstcommentary"><a id="SP12" class="paragraph-anchor"></a><b>&#167;12. </b>And this little function unpacks a list of KVDs into an array of values:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Latticework::unpack_kvd</span><span class="plain-syntax">(</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> **</span><span class="identifier-syntax">vals</span><span class="plain-syntax">, </span><span class="reserved-syntax">kind_variable_declaration</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kvd</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;27; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++) </span><span class="identifier-syntax">vals</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (; </span><span class="identifier-syntax">kvd</span><span class="plain-syntax">; </span><span class="identifier-syntax">kvd</span><span class="plain-syntax">=</span><span class="identifier-syntax">kvd</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">) </span><span class="identifier-syntax">vals</span><span class="plain-syntax">[</span><span class="identifier-syntax">kvd</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kv_number</span><span class="plain-syntax">] = </span><span class="identifier-syntax">kvd</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kv_value</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP13" class="paragraph-anchor"></a><b>&#167;13. Common code.</b>So the following routine tests conformance if <span class="extract"><span class="extract-syntax">comp</span></span> is <span class="extract"><span class="extract-syntax">FALSE</span></span>, returning
<span class="extract"><span class="extract-syntax">ALWAYS_MATCH</span></span> if and only if <span class="extract"><span class="extract-syntax">from</span></span> \(\leq\) <span class="extract"><span class="extract-syntax">to</span></span> holds; and otherwise it tests
compatibility, returning <span class="extract"><span class="extract-syntax">ALWAYS_MATCH</span></span>, <span class="extract"><span class="extract-syntax">SOMETIMES_MATCH</span></span> or <span class="extract"><span class="extract-syntax">NEVER_MATCH</span></span>
as appropriate.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Latticework::order_relation</span><button class="popup" onclick="togglePopup('usagePopup2')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup2">Usage of <span class="code-font"><span class="function-syntax">Latticework::order_relation</span></span>:<br/><a href="2-tlok.html#SP13_1">&#167;13.1</a>, <a href="2-tlok.html#SP13_4">&#167;13.4</a>, <a href="2-tlok.html#SP13_5_1">&#167;13.5.1</a>, <a href="2-tlok.html#SP13_5_2">&#167;13.5.2</a><br/>Kinds - <a href="2-knd.html#SP28">&#167;28</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">from</span><span class="plain-syntax">, </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">to</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP15" class="function-link"><span class="function-syntax">Kinds::get_variable_number</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">to</span><span class="plain-syntax">) &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">var_k</span><span class="plain-syntax"> = </span><span class="identifier-syntax">to</span><span class="plain-syntax">, *</span><span class="identifier-syntax">other_k</span><span class="plain-syntax"> = </span><span class="identifier-syntax">from</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP13_5" class="named-paragraph-link"><span class="named-paragraph">Deal separately with matches against kind variables</span><span class="named-paragraph-number">13.5</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP15" class="function-link"><span class="function-syntax">Kinds::get_variable_number</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">) &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">var_k</span><span class="plain-syntax"> = </span><span class="identifier-syntax">from</span><span class="plain-syntax">, *</span><span class="identifier-syntax">other_k</span><span class="plain-syntax"> = </span><span class="identifier-syntax">to</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP13_5" class="named-paragraph-link"><span class="named-paragraph">Deal separately with matches against kind variables</span><span class="named-paragraph-number">13.5</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP13_1" class="named-paragraph-link"><span class="named-paragraph">Deal separately with the sayability of lists</span><span class="named-paragraph-number">13.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP13_2" class="named-paragraph-link"><span class="named-paragraph">Deal separately with the top and bottom of the lattice</span><span class="named-paragraph-number">13.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP13_3" class="named-paragraph-link"><span class="named-paragraph">Deal separately with the special role of the unknown kind</span><span class="named-paragraph-number">13.3</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP13_4" class="named-paragraph-link"><span class="named-paragraph">The general case of compatibility</span><span class="named-paragraph-number">13.4</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP13_1" class="paragraph-anchor"></a><b>&#167;13.1. </b>A list is sayable if and only if it is empty, or its contents are sayable.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Deal separately with the sayability of lists</span><span class="named-paragraph-number">13.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="2-knd.html#SP14" class="function-link"><span class="function-syntax">Kinds::get_construct</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">) == </span><span class="identifier-syntax">CON_list_of</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax">        (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">to</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_sayable_value</span><span class="plain-syntax">))) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">CK</span><span class="plain-syntax"> = </span><a href="2-knd.html#SP17" class="function-link"><span class="function-syntax">Kinds::unary_construction_material</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">CK</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_nil</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">CK</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">; </span><span class="comment-syntax"> for an internal test case making dodgy lists</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="2-tlok.html#SP13" class="function-link"><span class="function-syntax">Latticework::order_relation</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">CK</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_sayable_value</span><span class="plain-syntax">, </span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP13">&#167;13</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP13_2" class="paragraph-anchor"></a><b>&#167;13.2. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Deal separately with the top and bottom of the lattice</span><span class="named-paragraph-number">13.2</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">to</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_value</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_nil</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP13">&#167;13</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP13_3" class="paragraph-anchor"></a><b>&#167;13.3. </b><span class="extract"><span class="extract-syntax">NULL</span></span> as a kind means "unknown". It's compatible only with itself
and, of course, "value".
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Deal separately with the special role of the unknown kind</span><span class="named-paragraph-number">13.3</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">to</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">from</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">to</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">from</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP13">&#167;13</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP13_4" class="paragraph-anchor"></a><b>&#167;13.4. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">The general case of compatibility</span><span class="named-paragraph-number">13.4</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">f_a</span><span class="plain-syntax"> = </span><a href="4-kc2.html#SP17" class="function-link"><span class="function-syntax">KindConstructors::arity</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">t_a</span><span class="plain-syntax"> = </span><a href="4-kc2.html#SP17" class="function-link"><span class="function-syntax">KindConstructors::arity</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">to</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">arity</span><span class="plain-syntax"> = (</span><span class="identifier-syntax">f_a</span><span class="plain-syntax"> &lt; </span><span class="identifier-syntax">t_a</span><span class="plain-syntax">)?</span><span class="identifier-syntax">f_a:t_a</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">o</span><span class="plain-syntax"> = </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax"> != </span><span class="identifier-syntax">to</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">o</span><span class="plain-syntax"> = </span><a href="2-tlok.html#SP15" class="function-link"><span class="function-syntax">Latticework::construct_compatible</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">, </span><span class="identifier-syntax">to</span><span class="plain-syntax">, </span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">, </span><span class="identifier-syntax">this_o</span><span class="plain-syntax"> = </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">, </span><span class="identifier-syntax">fallen</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;</span><span class="identifier-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="2-tlok.html#SP14" class="function-link"><span class="function-syntax">Latticework::vacuous</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">])) &amp;&amp; (</span><a href="2-tlok.html#SP14" class="function-link"><span class="function-syntax">Latticework::vacuous</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">to</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">])))</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">continue</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-kc2.html#SP17" class="function-link"><span class="function-syntax">KindConstructors::variance</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">i</span><span class="plain-syntax">) == </span><span class="constant-syntax">COVARIANT</span><span class="plain-syntax">)</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">this_o</span><span class="plain-syntax"> = </span><a href="2-tlok.html#SP13" class="function-link"><span class="function-syntax">Latticework::order_relation</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">to</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">this_o</span><span class="plain-syntax"> = </span><a href="2-tlok.html#SP13" class="function-link"><span class="function-syntax">Latticework::order_relation</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">to</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kc_args</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">switch</span><span class="plain-syntax"> (</span><span class="identifier-syntax">this_o</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH:</span><span class="plain-syntax"> </span><span class="identifier-syntax">o</span><span class="plain-syntax"> = </span><span class="identifier-syntax">this_o</span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">SOMETIMES_MATCH:</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">o</span><span class="plain-syntax"> != </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">) { </span><span class="identifier-syntax">o</span><span class="plain-syntax"> = </span><span class="identifier-syntax">this_o</span><span class="plain-syntax">; </span><span class="identifier-syntax">fallen</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; } </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">fallen</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">to</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax"> != </span><span class="identifier-syntax">CON_list_of</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">o</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP13">&#167;13</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP14" class="paragraph-anchor"></a><b>&#167;14. </b></p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Latticework::vacuous</span><button class="popup" onclick="togglePopup('usagePopup3')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup3">Usage of <span class="code-font"><span class="function-syntax">Latticework::vacuous</span></span>:<br/><a href="2-tlok.html#SP13_4">&#167;13.4</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_nil</span><span class="plain-syntax">)) || (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_void</span><span class="plain-syntax">))) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP15" class="paragraph-anchor"></a><b>&#167;15. </b></p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Latticework::construct_compatible</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">Latticework::construct_compatible</span></span>:<br/><a href="2-tlok.html#SP13_4">&#167;13.4</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">from</span><span class="plain-syntax">, </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">to</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">from</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">while</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">to</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="2-tlok.html#SP6" class="function-link"><span class="function-syntax">Latticework::super</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">) &amp;&amp; (</span><a href="4-kc2.html#SP20" class="function-link"><span class="function-syntax">KindConstructors::find_cast</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">, </span><span class="identifier-syntax">to</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">construct</span><span class="plain-syntax">)))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">to</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">while</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP27" class="function-link"><span class="function-syntax">Kinds::eq</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">from</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">HIERARCHY_ALLOWS_SOMETIMES_MATCH_KINDS_CALLBACK</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">HIERARCHY_ALLOWS_SOMETIMES_MATCH_KINDS_CALLBACK</span><span class="plain-syntax">(</span><span class="identifier-syntax">from</span><span class="plain-syntax">))</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">SOMETIMES_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">            #</span><span class="identifier-syntax">ifndef</span><span class="plain-syntax"> </span><span class="identifier-syntax">HIERARCHY_ALLOWS_SOMETIMES_MATCH_KINDS_CALLBACK</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">SOMETIMES_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="2-tlok.html#SP6" class="function-link"><span class="function-syntax">Latticework::super</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP13_5" class="paragraph-anchor"></a><b>&#167;13.5. </b>Recall that kind variables are identified by a number in the range 1 ("A")
to 26 ("Z"), and that it is also possible to assign them a domain, or a
"declaration". This marks that they are free to take on a value, within
that domain. For example, in
</p>

<blockquote>
    <p>To add (new entry - K) to (L - list of values of kind K) ...</p>
</blockquote>

<p class="commentary">the first appearance of <span class="extract"><span class="extract-syntax">K</span></span> will be an ordinary use of a kind variable,
whereas the second has the declaration <span class="extract"><span class="extract-syntax">value</span></span> &mdash; meaning that it can
become any kind matching <span class="extract"><span class="extract-syntax">value</span></span>. (It could alternatively have had a
more restrictive declaration like <span class="extract"><span class="extract-syntax">arithmetic value</span></span>.)
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Deal separately with matches against kind variables</span><span class="named-paragraph-number">13.5</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">switch</span><span class="plain-syntax">(</span><span class="identifier-syntax">kind_checker_mode</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">MATCH_KIND_VARIABLES_AS_SYMBOLS:</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP15" class="function-link"><span class="function-syntax">Kinds::get_variable_number</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">other_k</span><span class="plain-syntax">) ==</span>
<span class="plain-syntax">                </span><a href="2-knd.html#SP15" class="function-link"><span class="function-syntax">Kinds::get_variable_number</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">var_k</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">MATCH_KIND_VARIABLES_AS_UNIVERSAL:</span><span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">default:</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">vn</span><span class="plain-syntax"> = </span><a href="2-knd.html#SP15" class="function-link"><span class="function-syntax">Kinds::get_variable_number</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">var_k</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-knd.html#SP15" class="function-link"><span class="function-syntax">Kinds::get_variable_stipulation</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">var_k</span><span class="plain-syntax">))</span>
<span class="plain-syntax">                </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP13_5_1" class="named-paragraph-link"><span class="named-paragraph">Act on a declaration usage, where inference is allowed</span><span class="named-paragraph-number">13.5.1</span></a></span>
<span class="plain-syntax">            </span><span class="reserved-syntax">else</span>
<span class="plain-syntax">                </span><span class="named-paragraph-container code-font"><a href="2-tlok.html#SP13_5_2" class="named-paragraph-link"><span class="named-paragraph">Act on an ordinary usage, where inference is not allowed</span><span class="named-paragraph-number">13.5.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP13">&#167;13</a> (twice).</li></ul>
<p class="commentary firstcommentary"><a id="SP13_5_1" class="paragraph-anchor"></a><b>&#167;13.5.1. </b>When the specification matcher works on matching text such as
</p>

<blockquote>
    <p>add 23 to the scores list;</p>
</blockquote>

<p class="commentary">it works through the prototype:
</p>

<blockquote>
    <p>To add (new entry - K) to (L - list of values of kind K) ...</p>
</blockquote>

<p class="commentary">in two passes. On the first pass, it tries to match the tokens "23" and
"scores list" against <span class="extract"><span class="extract-syntax">K</span></span> and <span class="extract"><span class="extract-syntax">list of values of kind K</span></span> respectively
in <span class="extract"><span class="extract-syntax">MATCH_KIND_VARIABLES_INFERRING_VALUES</span></span> mode; on the second pass, it
does the same in <span class="extract"><span class="extract-syntax">MATCH_KIND_VARIABLES_AS_VALUES</span></span> mode. In this example,
on the first pass we infer (from the kind of "scores list", which is
indeed a list of numbers) that <span class="extract"><span class="extract-syntax">K</span></span> must be <span class="extract"><span class="extract-syntax">number</span></span>; on the second pass
we verify that "23" is a <span class="extract"><span class="extract-syntax">K</span></span>.
</p>

<p class="commentary">The following shows what happens matching <span class="extract"><span class="extract-syntax">values of kind K</span></span>, which is
a declaration usage of the variable <span class="extract"><span class="extract-syntax">K</span></span>.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Act on a declaration usage, where inference is allowed</span><span class="named-paragraph-number">13.5.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">switch</span><span class="plain-syntax">(</span><span class="identifier-syntax">kind_checker_mode</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">MATCH_KIND_VARIABLES_INFERRING_VALUES:</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-tlok.html#SP13" class="function-link"><span class="function-syntax">Latticework::order_relation</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">other_k</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                </span><a href="2-knd.html#SP15" class="function-link"><span class="function-syntax">Kinds::get_variable_stipulation</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">var_k</span><span class="plain-syntax">), </span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">) != </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">KIND_CHECKING</span><span class="plain-syntax">, </span><span class="string-syntax">"Inferring kind variable %d from %u (declaration %u)\n"</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">vn</span><span class="plain-syntax">, </span><span class="identifier-syntax">other_k</span><span class="plain-syntax">, </span><a href="2-knd.html#SP15" class="function-link"><span class="function-syntax">Kinds::get_variable_stipulation</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">var_k</span><span class="plain-syntax">));</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">values_of_kind_variables</span><span class="plain-syntax">[</span><span class="identifier-syntax">vn</span><span class="plain-syntax">] = </span><span class="identifier-syntax">other_k</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">kind_variable_declaration</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kvd</span><span class="plain-syntax"> = </span><span class="identifier-syntax">CREATE</span><span class="plain-syntax">(</span><span class="reserved-syntax">kind_variable_declaration</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">kvd</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kv_number</span><span class="plain-syntax"> = </span><span class="identifier-syntax">vn</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">kvd</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">kv_value</span><span class="plain-syntax"> = </span><span class="identifier-syntax">other_k</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">kvd</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">MATCH_KIND_VARIABLES_AS_VALUES:</span><span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP13_5">&#167;13.5</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP13_5_2" class="paragraph-anchor"></a><b>&#167;13.5.2. </b>Whereas this is what happens when matching just <span class="extract"><span class="extract-syntax">K</span></span>. On the inference pass,
we always make a match, which is legitimate because we know we are going to
make a value-checking pass later.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Act on an ordinary usage, where inference is not allowed</span><span class="named-paragraph-number">13.5.2</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">switch</span><span class="plain-syntax">(</span><span class="identifier-syntax">kind_checker_mode</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">MATCH_KIND_VARIABLES_INFERRING_VALUES:</span><span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">MATCH_KIND_VARIABLES_AS_VALUES:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">KIND_CHECKING</span><span class="plain-syntax">, </span><span class="string-syntax">"Checking %u against kind variable %d (=%u)\n"</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">other_k</span><span class="plain-syntax">, </span><span class="identifier-syntax">vn</span><span class="plain-syntax">, </span><span class="identifier-syntax">values_of_kind_variables</span><span class="plain-syntax">[</span><span class="identifier-syntax">vn</span><span class="plain-syntax">]);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-tlok.html#SP13" class="function-link"><span class="function-syntax">Latticework::order_relation</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">other_k</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">values_of_kind_variables</span><span class="plain-syntax">[</span><span class="identifier-syntax">vn</span><span class="plain-syntax">], </span><span class="identifier-syntax">allow_casts</span><span class="plain-syntax">) == </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">else</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="2-tlok.html#SP13_5">&#167;13.5</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP16" class="paragraph-anchor"></a><b>&#167;16. </b>It's easy to confused when writing a type checker, especially with variables
getting in the way, so these logging functions can be helpful:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Latticework::show_variables</span><span class="plain-syntax">(</span><span class="reserved-syntax">void</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Variables: "</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=1; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;=26; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">values_of_kind_variables</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">];</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">continue</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"%c=%u "</span><span class="plain-syntax">, </span><span class="character-syntax">'A'</span><span class="plain-syntax">+</span><span class="identifier-syntax">i</span><span class="plain-syntax">-1, </span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"\n"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Latticework::show_frame_variables</span><span class="plain-syntax">(</span><span class="reserved-syntax">void</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">shown</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=1; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;=26; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="2-knd.html#SP26" class="function-link"><span class="function-syntax">Kinds::variable_from_context</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">i</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">shown</span><span class="plain-syntax">++ == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">MATCHING</span><span class="plain-syntax">, </span><span class="string-syntax">"Stack frame uses kind variables: "</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">MATCHING</span><span class="plain-syntax">, </span><span class="string-syntax">"%c=%u "</span><span class="plain-syntax">, </span><span class="character-syntax">'A'</span><span class="plain-syntax">+</span><span class="identifier-syntax">i</span><span class="plain-syntax">-1, </span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">shown</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">MATCHING</span><span class="plain-syntax">, </span><span class="string-syntax">"Stack frame sets no kind variables"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">MATCHING</span><span class="plain-syntax">, </span><span class="string-syntax">"\n"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<nav role="progress"><div class="progresscontainer">
    <ul class="progressbar"><li class="progressprev"><a href="2-fk.html">&#10094;</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-km.html">1</a></li><li class="progresscurrentchapter">2</li><li class="progresssection"><a href="2-knd.html">knd</a></li><li class="progresssection"><a href="2-fk.html">fk</a></li><li class="progresscurrent">tlok</li><li class="progresssection"><a href="2-dk.html">dk</a></li><li class="progresssection"><a href="2-uk.html">uk</a></li><li class="progresschapter"><a href="3-dmn.html">3</a></li><li class="progresschapter"><a href="4-abgtn.html">4</a></li><li class="progressnext"><a href="2-dk.html">&#10095;</a></li></ul></div>
</nav><!-- End of weave -->

		</main>
	</body>
</html>

